package no.uio.ifi.cop.prover.cmp;

import java.util.Comparator;

import no.uio.ifi.cop.prover.RuleMatcher;
import no.uio.ifi.cop.cl.Axiom;


/**
 * Natural ordering, that takes number of applications
 * into account.
 *
 * @version 1.0
 * @author bjarneh@ifi.uio.no
 */

public class ExistPreference implements Comparator<RuleMatcher>{

    public int compare(RuleMatcher first, RuleMatcher second){

        int firstType, secondType;

        if( first == second ){ return 0; }

        firstType   = first.getAxiom().getType();
        secondType  = second.getAxiom().getType();

        if( first.getId() == second.getId() ){ return 0; }

        if( firstType == secondType ){
            return (first.getId() < second.getId())? -1 : 1;
        }

        if( firstType == Axiom.EXISTRULE ){
            if( secondType == Axiom.DISJUNCTRULE ){
                return -1;
            }
        }else if( secondType == Axiom.EXISTRULE ){
            if( firstType == Axiom.DISJUNCTRULE ){
                return 1;
            }
        }

        
        return (firstType < secondType)? -1 : 1;
    }
}
